A:MsgA, x:Id, k:Knd.
Feasible(A)  (<k, x>  dom((A.2.2.2.2).1) = tt  )  A.aframe(k affects x) 

latex

Definitions

x:A. B(x), P & Q, b, t  T, Id, x:A  B(x), Knd, x:AB(x), S  T, P  Q, IdLnk, P  Q, Void, Type, x.A(x), x. t(x), t.2, IdDeq, f(x)?z, Top, t.1, KindDeq, State(ds), a:A fp B(a), tt, product-deq(A;B;a;b), x  dom(f), , s = t, , type List, z != f(x)  P(a;z), xdom(f). v=f(x)   P(x;v), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), Valtype(da;k), MsgA, Feasible(M), <a, b>

Lemmas

msga wf, ma-feasible wf, bool wf, fpf-dom wf, product-deq wf, btrue wf, fpf-trivial-subtype-top, ma-state wf, Kind-deq wf, pi1 wf, top wf, fpf-cap wf, id-deq wf, pi2 wf, Knd wf, Id wf, eqtt to assert